
% ------------------------------------------------------------------------------
%  Header                                                                       
% ------------------------------------------------------------------------------

\documentclass[svgnames]{beamer} % pass svgnames to xcolor
\usetheme[titleline=true]{Torino}
% \setbeamercolor{title}{fg=red!80!black}
\setbeamertemplate{footline}[frame number]

\usepackage{hyperref} 
\usepackage{proof}
\usepackage{graphicx}
\usepackage[overlay,absolute]{textpos}

\usepackage{tikz}
\usetikzlibrary{arrows,shapes,calc}

% ------------------------------------------------------------------------------
%  Commands                                                                     
% ------------------------------------------------------------------------------

\newcommand{\Rsize}{$\footnotesize$}
\renewcommand{\And}{\wedge}
\newcommand{\Not}{\neg}
\newcommand{\Or}{\vee}
\newcommand{\Imp}{\supset}
\newcommand{\Bot}{\bot}
\newcommand{\Top}{\top}
\newcommand{\Seq}[2]{#1 \vdash #2}

\newcommand{\TalkColor}{chameleongreen3}
\newcommand{\PartColor}{chameleongreen4}
\newcommand{\Space}{\hspace{1.4cm}}

\newcommand{\textframe}[1]{
  \begin{frame}   
    \begin{center}         
      {\color{\TalkColor} \Huge #1}
    \end{center} 
  \end{frame} 
}

\newcommand{\imgframe}[2]{
  \begin{frame}   
    \begin{center}         
      \includegraphics[scale=#1]{#2}
    \end{center} 
  \end{frame} 
}

\newcommand{\Init}{\Rsize $Init$}
\newcommand{\AndR}{\Rsize \And$-R$}
\newcommand{\AndLa}{\Rsize \And$-L$_1}
\newcommand{\AndLb}{\Rsize \And$-L$_2}
\newcommand{\AllR}{\Rsize \forall$-R$}
\newcommand{\Sep}{\ |\ }

% ------------------------------------------------------------------------------
%  Begin                                                                        
% ------------------------------------------------------------------------------

\begin{document}

% ------------------------------------------------------------------------------

\begin{frame} 
  \begin{center} 
    {\huge \color{chameleongreen3}
      Functional Programming \\[.5ex] 
       and HOL Light
    }

    \vspace{.7cm}

    {\Large
      Sean McLaughlin and Roland Zumkeller
    }

    \bigskip 
  \end{center} 
\end{frame} 

% ------------------------------------------------------------------------------

\imgframe{.5}{images/cannon.jpg}

% % ------------------------------------------------------------------------------

% \imgframe{.5}{images/miracle.png}

% ------------------------------------------------------------------------------

\imgframe{.3}{images/frege.jpg}

% ------------------------------------------------------------------------------

\imgframe{.3}{images/pric.png}

% ------------------------------------------------------------------------------

\imgframe{.3}{images/russell.jpg}

% ------------------------------------------------------------------------------

\textframe{Example}

% ------------------------------------------------------------------------------

\begin{frame}{Language} 

  \Large

  \tikzstyle{every picture}+=[remember picture]
%  \tikzstyle{na} = [baseline=-.5ex]
  \tikzstyle{na} = []

  \begin{overlayarea}{\textwidth}{3cm} 

    \begin{align*} 
      \mbox{Formulas } A ::= p \Sep A_1\tikz[na] \coordinate (mvar1); \And A_2\tikz[na] \coordinate (mvar2); \Sep (\ \tikz[na] \coordinate (mvar3); A\ ) 
    \end{align*} 

  \end{overlayarea} 

%   \vspace{2cm}

  \begin{overlayarea}{\textwidth}{3cm} 

    \only<1>{
      \vspace{-1cm}
      \[
      \begin{array}{c}
        p_1 \And p_2 \And p_3 
        \\
        (p_1 \And p_2) \And (p_2 \And p_1)
        \\
        \vdots
      \end{array} 
      \]
    }

    \only<2->{
      \begin{center} 
        \tikz[na] \coordinate[label=below:{Meta-variables}] (Mvar);
      \end{center}  

      \begin{tikzpicture}[overlay, very thick, >=open triangle 45]
        \path[chameleongreen3, ->] (Mvar.north) edge ($(mvar1.south) - (.3,.1)$);
        \path[chameleongreen3, ->] (Mvar.north) edge ($(mvar2.south) - (.3,.1)$);
        \path[chameleongreen3, ->] (Mvar.north) edge ($(mvar3.south) - (-.1,.1)$);
      \end{tikzpicture}
    }

  \end{overlayarea} 

\end{frame} 

% ------------------------------------------------------------------------------

\begin{frame}{Proofs}

  \Large

  \vspace{-1cm}
  \[
  \mbox{Sequents} ::= \Seq{\Gamma}{A}
  \]

  \bigskip 

  \[
  \begin{tabular}{c@{\Space}c}
    \infer[\Init]
    {\Seq{\Gamma, A}{A}}
    {}
    &
    \infer[\AndR]
    {\Seq{\Gamma}{A\And B}}
    {\Seq{\Gamma}{A} & \Seq{\Gamma}{B}}
    \\[2em]
    \infer[\AndLa]
    {\Seq{\Gamma, A\And B}{C}}
    {\Seq{\Gamma, A}{C}}
    &
    \infer[\AndLb]
    {\Seq{\Gamma, A\And B}{C}}
    {\Seq{\Gamma, B}{C}}
  \end{tabular} 
  \]

\end{frame} 

% ------------------------------------------------------------------------------

\begin{frame}{Proof Checking}

  \Large

  \bigskip 

  \begin{overlayarea}{\textwidth}{3cm} 
    \[
    \infer[$\alert<2->{$\AndR$}$]
    {\alert<2->{\Seq{p\And q}{q \And p}}}
    {
      \infer[\AndLb]
      {\alert<2->{\Seq{p\And q}{q}}}
      {\infer[\Init]
        {\Seq{q}{q}}
        {}
      }
      &
      \infer[\AndLa]
      {\alert<2->{\Seq{p\And q}{p}}}
      {\infer[\Init]
        {\Seq{p}{p}}
        {}
      }
    }
    \]
  \end{overlayarea} 

  \begin{overlayarea}{\textwidth}{3cm} 

    \only<1-2>{
      \invisible<1-2>{
        \[
        \infer[\AndR]
        {\Seq{\Gamma}{A\And B}}
        {\Seq{\Gamma}{A} & \Seq{\Gamma}{B}}
        \]
      }
    }

    \only<3>{
      \[
      \infer[\AndR]
      {\Seq{\Gamma}{A\And B}}
      {\Seq{\Gamma}{A} & \Seq{\Gamma}{B}}
      \]
    }

    \only<4>{
      \[
      \infer[\AndR]
      {\Seq{\alert{\Gamma}}{A\And B}}
      {\Seq{\alert{\Gamma}}{A} & \Seq{\alert{\Gamma}}{B}}
      \]
    }

    \only<5>{
      \[
      \infer[\AndR]
      {\Seq{\alert{p\And q}}{A\And B}}
      {\Seq{\alert{p\And q}}{A} & \Seq{\alert{p\And q}}{B}}
      \]
    }

    \only<6>{
      \[
      \infer[\AndR]
      {\Seq{p\And q}{\alert{A}\And B}}
      {\Seq{p\And q}{\alert{A}} & \Seq{p\And q}{B}}
      \]
    }

    \only<7>{
      \[
      \infer[\AndR]
      {\Seq{p\And q}{\alert{q}\And B}}
      {\Seq{p\And q}{\alert{q}} & \Seq{p\And q}{B}}
      \]
    }

    \only<8>{
      \[
      \infer[\AndR]
      {\Seq{p\And q}{q\And \alert{B}}}
      {\Seq{p\And q}{q} & \Seq{p\And q}{\alert{B}}}
      \]
    }

    \only<9>{
      \[
      \infer[\AndR]
      {\Seq{p\And q}{q\And \alert{p}}}
      {\Seq{p\And q}{p} & \Seq{p\And q}{\alert{p}}}
      \]
    }

  \end{overlayarea} 

\end{frame} 

% ------------------------------------------------------------------------------

\begin{frame}{Proof Checking} 

  \Large 

  \begin{overlayarea}{\textwidth}{3cm} 
    \[
    \infer[\AndR]
    {\Seq{\alert{p\And p}}{q \And p}}
    {
      \infer[\AndLb]
      {\Seq{p\And q}{q}}
      {\infer[\Init]
        {\Seq{q}{q}}
        {}
      }
      &
      \infer[\AndLa]
      {\Seq{p\And q}{p}}
      {\infer[\Init]
        {\Seq{p}{p}}
        {}
      }
    }
    \]
  \end{overlayarea} 

  \begin{overlayarea}{\textwidth}{3cm} 

  \end{overlayarea} 

\end{frame} 

% ------------------------------------------------------------------------------


\begin{frame}{Proof Checking} 

  \Large

  \[
  \infer[\AllR]
  {\Seq{\Gamma}{\forall x. A(x)}}
  {
    \Seq{\Gamma}{A(x)} 
    & 
    x \not\in \Gamma
  }
  \]

\end{frame} 

% ------------------------------------------------------------------------------

\newcommand{\ColorA}{\color{Navy}}
\newcommand{\ColorB}{\color{chameleongreen3}}

\begin{frame}

  \huge

  \only<1-4>{
    \begin{center} 
      \begin{tabular}{c} 
        \only<1>{\ColorA Language}
        \only<2->{\ColorB Simple type theory (HOL)}
        \\[2em]
        \only<1-2>{\ColorA Meta-language}
        \only<3->{\ColorB Objective Caml (OCaml)}
        \\[2em]
        \only<1-3>{\ColorA Computation}
        \only<4>{\ColorB Functional programs}
      \end{tabular} 
    \end{center} 
  }

  \only<5>{
    \begin{center} 
      \begin{tabular}{c}
        \ColorB      
        {\Huge HOL Light = HOL + OCaml }
      \end{tabular} 
    \end{center} 
  }  
  
\end{frame} 

% ------------------------------------------------------------------------------

\begin{frame}

\begin{itemize} 
\item Why HOL Light?
  \begin{itemize} 
  \item Small trusted core 
  \item Highly customizable, extendible
  \item Advanced analysis libraries
  \end{itemize} 
  \medskip 
\item Why OCaml?
  \begin{itemize} 
  \item Meta-Language of HOL Light
  \item Strong types, higher-order functions, module system
  \item Efficient compiler
  \end{itemize} 
\end{itemize} 

\end{frame} 

% ------------------------------------------------------------------------------

\begin{frame}

  \Large

  \[
  \infer[\AndR]
  {\Seq{p\And q}{q \And p}}
  {
    \infer[\AndLb]
    {\Seq{p\And q}{q}}
    {\infer[\Init]
      {\Seq{q}{q}}
      {}
    }
    &
    \infer[\AndLa]
    {\Seq{p\And q}{p}}
    {\infer[\Init]
      {\Seq{p}{p}}
      {}
    }
  }
  \]

  \begin{center} 
    \includegraphics[scale=.5]{images/hol.png}
  \end{center} 

\end{frame} 

% ------------------------------------------------------------------------------

\begin{frame}{Tactics}

  \Large 

  \[
  \infer[\AndLa]
  {\Seq{\Gamma, A\And B}{C}}
  {\Seq{\Gamma, A}{C}}
  \]

  \medskip 

  \begin{center} 
    \includegraphics[scale=.5]{images/tac.png}
  \end{center} 

\end{frame} 

% ------------------------------------------------------------------------------

\begin{frame}{Automation}
  \begin{center} 
    \includegraphics[scale=.5]{images/rqe.png}
  \end{center} 
\end{frame} 

% ------------------------------------------------------------------------------

\begin{frame}{101,359 inference rule applications}
  \begin{center} 
    \includegraphics[scale=.3]{images/arith.png}
  \end{center} 
\end{frame} 

% ------------------------------------------------------------------------------

\textframe{Courses}

% ------------------------------------------------------------------------------

\begin{frame}{Courses}

  \large

  \tikzstyle{every picture}+=[remember picture]
  \tikzstyle{na} = [baseline=-.5ex]

  \begin{columns} 

    \begin{column}{.4\textwidth} 
      {\Large \ColorA Functional Prog.}
      \medskip 
      \begin{itemize} 
      \item Lambda calculus \tikz[na] \coordinate (lam);
      \item Types \tikz[na] \coordinate (typ);
      \item Data structures \tikz[na] \coordinate (dat);
      \item Algorithms \tikz[na] \coordinate (alg);
      \item Module system \tikz[na] \coordinate (mod);
      \end{itemize}
    \end{column} 

    \begin{column}{.4\textwidth} 
      {\Large \ColorA HOL Light}
      \medskip 
      \begin{itemize} 
      \item \tikz[na] \coordinate (ker);Logical kernel
      \item Logical encodings
      \item Forward proof
      \item Backward proof
      \item \tikz[na] \coordinate (auto);Automation 
      \end{itemize} 
    \end{column} 

  \end{columns} 

  \begin{tikzpicture}[overlay, very thick, >=open triangle 45]

    \uncover<2>{
      \path[red, ->] (typ) edge (ker);
      \path[red, ->] (mod) edge (ker);
    }
    \uncover<3->{
      \path[blue, ->] (typ) edge (ker);
      \path[blue, ->] (mod) edge (ker);
    }

    \uncover<3>{
      \path[red, ->] (ker) edge (lam);
      \path[red, ->] (ker) edge (typ);
    }
    \uncover<4->{
      \path[blue, ->] (ker) edge (lam);
      \path[blue, ->] (ker) edge (typ);
    }

    \uncover<4>{
      \path[red, ->] (dat) edge (auto);
      \path[red, ->] (alg) edge (auto);
    }
    \uncover<5->{
      \path[blue, ->] (dat) edge (auto);
      \path[blue, ->] (alg) edge (auto);
    }

  \end{tikzpicture}

\end{frame} 

% ------------------------------------------------------------------------------

\begin{frame}{Format}

  \begin{itemize} 

  \item Tools
    \begin{itemize} 
    \item Linux
    \item Emacs
    \end{itemize} 
    \medskip 

  \item OCaml
    \begin{itemize} 
    \item 2 hours lecture, 4 hours lab per week
    \item Lots of short exercises
    \item Programming project 
    \end{itemize} 
    \medskip 

  \item HOL Light
    \begin{itemize} 
    \item No lectures.  Short presentations during labs
    \item 8 hours lab per week
    \item Lots of exercises (theorems)
    \end{itemize} 

  \end{itemize} 

\end{frame} 

% ------------------------------------------------------------------------------

\begin{frame}{Goals}

  \ColorA

  \Large

  \begin{center} 
    \begin{tabular}{c}
      Prove theorems in HOL Light
      \\[2em]
      Automate repetitive HOL Light tasks with OCaml
      \\[2em]
      Write beautiful functional programs
    \end{tabular} 
  \end{center} 

\end{frame} 

% ------------------------------------------------------------------------------

\imgframe{.4}{images/kepler.png}

% ------------------------------------------------------------------------------

\textframe{Questions?}

% ------------------------------------------------------------------------------
%  End                                                                          
% ------------------------------------------------------------------------------
 
\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 
